A picture of Yoichi Hirai, wearing a suit, and smiling.

Yoichi Hirai (平井洋一)

interests

  • Computation and some logics
  • Becoming a "convenience logician" in the sense of "convenience stores"

resume

DBLP

contact information

prizes, grants and distinctions

  • 科研費(研究活動スタート支援) 交付内定 2013--2015.
  • PPL2013 presentation award.
  • JSPS Research Fellowships for Young Scientists. 2011--2013.
  • 平成21年度国家公務員採用Ⅰ種試験合格(名簿は有効期限切れ)
  • Dean's Award of Graduate School of Information Science and Technology, The University of Tokyo,
    東京大学大学院 情報理工学系研究科 研究科長賞, 2010.
  • Classified among the 20 best candidates in Japanese Mathematical Olympiad. 2002.

publication

refereed

  • Yoichi Hirai: Defining the Ethereum Virtual Machine for Interactive Theorem Provers (paper slides), 1st Workshop on Trusted Smart Contracts, 2017, accepted
  • Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, César Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews and Thomas Tuerk. Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor, FM 2016
  • Alessandro Facchini, Yoichi Hirai, Maarten Marx, and Evgeny Sherkhonov: Containment for conditional tree patterns. Logical Methods in Computer Science, 2015.
  • Yoichi Hirai, Reynald Affeldt: What can Coq do for Database Software? ---A Progress Report, JFLA 2014
  • Yoichi Hirai: Session Types in Abelian Logic, accepted to PLACES'13.
  • Yoichi Hirai: A Lambda Calculus for Gödel-Dummett Logic Capturing Waitfreedom, FLOPS 2012, LNCS 7294, pp. 151-165 (draft slide).
  • Kosuke Ono, Yoichi Hirai, Masami Hagiya, Natsuko Noda and Yoshinori Tanabe: Using Coq in Specification and Program Extraction of Hadoop MapReduce Applications, SEFM'11, 2011.
  • Yoichi Hirai and Kazuhiko Yamamoto: Balancing Weight-Balanced Trees. Journal of Functional Programming, volume 21, issue 03, pp. 287-307. 2011. (project page, local PDF)
  • Yoichi Hirai: An Intuitionistic Epistemic Logic for Sequential Consistency on Shared Memory. LPAR-16. 2010.
    paper (PDF) (The original version is available at www.springerlink.com)
    slide
  • 平井洋一「逐次一貫性下の知識伝達を表す直観主義様相論理」(PPL2010 カテゴリ1) 論文(pdf) スライド(pdf)

theses

  • Yoichi Hirai: Duality between Nondeterminism and Concurrency on Generalized Petri Net, Bachelor's Thesis, 2008 (pdf).
  • Yoichi Hirai: An Intuitionistic Epistemic Logic for Asynchronous Communication, Master's Thesis, 2010 (pdf).
  • Yoichi Hirai: Hyper-Lambda Calculi, Doctoral Thesis, 2013 (pdf).

unrefereed

  • Reasonable Manifesto
  • 平井洋一「分散プログラムを形式的証明から抽出する」 日本ソフトウェア科学会第26回大会で当日配布した修正版(pdf)． (スライド(pdf))
  • 平井洋一「線形論理に基づく論理式=型=プロトコルの言語」(日本ソフトウェア科学会大会2008)

talks

  • Yoichi Hirai: Blockchains as Kripke Models: an Analysis of Atomic Cross-Chain Swap (Limassol 2018-11-05) slide draft
  • Yoichi Hirai: Morphing Smart Contracts with Bamboo (Cancun 2017-11-02) (slide)
  • Yoichi Hirai: Verifying Casper (Cancun 2017-11-01) (slides)
  • Yoichi Hirai: Specifying the Ethereum Virtual Machine for Theorem Provers (Cambridge 2017-09-13) (slides)
  • Yoichi Hirai: Isabelle/HOL on Fork Prevention in the Coming Ethereum Protocol (Berlin 2017-08-30) (slides)
  • Yoichi Hirai: Interactive theorem proving in the Ethereum project (Garching by Munich 2017-05-31) (slide)
  • Yoichi Hirai: Formal Verification for Ethereum (Amsterdam 2017-05-03) (slides video)
  • Yoichi Hirai: Blockchains: new home for proven-correct software (Paris 2017-02-17) (slide Video)
  • Yoichi Hirai: formal verification of smart contracts (Ethereum Meetup Berlin 2016-11-01).
  • 平井洋一: Formalizing Surreal Numbers and Combinatorial Games (第11回論理と計算セミナー)
  • 平井洋一「形式検証によるコマンド・インジェクション攻撃対策」 (日本応用数理学会2013年度年会 研究部会OS: 数理的技法による情報セキュリティ)
  • Session Types in Abelian Logic, PPL2013, 2013.
  • Hyper-Lambda Calculi, LOng Seminar, Oxford, 2013.
  • 提題「ゲーデル・ダメット論理における情報フロー」(科学基礎論学会2012年度講演会、学会特別企画ワークショップ「情報・時間・論理」), 東京都, 2012.
  • A. Facchini, Y. Hirai, M. Marx, E. Shekhernov: Containment for higher order tree patterns, FOX Closing Event, 2012.
  • Yoichi Hirai wants to be a traveling merchant at student session of OPLSS 2011.
  • Yoichi Hirai: Hyper-lambda calculus for waitfree computation: theory and implementation at ACAN workshop, 2011.
  • Yoichi Hirai: Determining the Valid Parameters for the Weight-Balanced Tree Algorithm at The 4th DIKU-IST Joint Workshop, 2011.
  • poster (Japanese) for an interview of DC2 fellowship of JSPS
  • Yoichi Hirai (speaker), Kazuhiko Yamamoto: Balance Condition on Weight-Balanced Trees at TPP'10
  • Yoichi Hirai: Disjunction Property and Finite Model Property For an Intuitionistic Epistemic Logic (NASSLLI2010 student session) (slide (pdf), paper).
  • 平井洋一「トートロジーの中で代入極小でない中間論理の公理」(PPL 2009, カテゴリ3)
  • 平井洋一「線形論理の証明としてメモリを書く」(CSCAT 2008) 口頭
  • 平井洋一「Prover-skeptic Dialogue for MALL」(SLACS2008)
  • 平井洋一「Generalizing Rationalizability in the Modal Mu-Calculus」
  • 平井洋一「論理学的にみたゲーム理論のプレイヤー」(東京財団VCASIインフォーマルセミナー)

teaching experiences

  • Summer 2008: TA for logic excersise class.
  • Summer 2009: TA for logic excersise class.
  • Summer 2010: TA for logic excersise class.

former positions

  • An engineer at BedRock Systems, Inc (2020--2024)
  • An engineer at brainbot technologies AG (2018--2019)
  • A formal verification engineer at Ethereum DEV UG (2016--2018)
  • A formal verification engineer at FireEye Technologie Deutschland (2014--2016)
  • A researcher at AIST (2013--2014)
  • A PhD student, advised by Prof. Masami Hagiya in Dept. of Computer Science, the University of Tokyo
  • A visiting student, ILPS, the University of Amsterdam

misc

This page is powered by bootstrap framework.

This website is hosted on GitLab Pages. GitLab might be obtaining your IP address and other information, so please refer to GitLab Privacy Statement.